COMMENT ⊗   VALID 00006 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(wipe-out)
C00010 00003	 ekl axioms and proofs for permutation functions
C00014 00004	facts on append
C00016 00005	facts on reverse: these do the facts mentioned in our meeting for reverse
C00020 00006	properties of rac,rdc,snoc,lcycle,rcycle
C00032 ENDMK
C⊗;
(wipe-out)
(proof lispax) 

;;;declarations: note that t and nil are not declared - ekl knows about them
;;;since they are attached, we don't need to say things like null nil etc.

(decl car (unaryname: car) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl cdr (unaryname: cdr) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl atom (unaryname: atom) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl null (unaryname: null) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl listp (unaryname: listp) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl alistp (unaryname: alistp) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl sexp (unaryname: sexp) (type: |ground→truthval|) (syntype: constant)
 (bindingpower: 750))

(decl (u v w) (type: |ground|) (sort: |listp|))

(decl (x y z) (type: |ground|) (sort: |sexp|))

(decl (xa ya za) (type: |ground|) (sort: |atom|))

(decl (a b c) (type: |ground|))

(decl (phi) (type: |ground→truthval|))

(decl cons (type: |(ground⊗ground)→ground|) (syntype: constant) (infixname: |.|)
 (prefixname: cons) (bindingpower: 850))

;;;basic axioms and sort info

(axiom |∀xa.sexp(xa)|)
(label simpinfo)

(axiom |∀u.sexp u|)
(label simpinfo)

(axiom |∀x u.listp x.u|)
(label simpinfo)

(axiom |∀u.¬null u ⊃ listp cdr u|)
(label simpinfo)

(axiom |∀u.¬null u ⊃ sexp car u|)
(label simpinfo)

(axiom |∀x.¬atom x ⊃ sexp car x|)
(label simpinfo)

(axiom |∀x.¬atom x ⊃ sexp cdr x|)
(label simpinfo)

(axiom |∀u.u=nil ≡ null u|)
(label simpinfo)
(axiom |∀u.nil=u ≡ null u|)
(label simpinfo)

(axiom |∀x y.sexp x.y|)
(label simpinfo)

(axiom |∀x y.¬atom x.y|)
(label simpinfo)

(axiom |∀x u.¬null x.u|)
(label simpinfo)

(axiom |∀x y.car (x.y) = x|)
(label simpinfo)

(axiom |∀x y.cdr (x.y) = y|)
(label simpinfo)

(axiom |∀u.¬null u ⊃ (car u.cdr u=u)|)
(label simpinfo)

(axiom |∀x.¬atom x ⊃ (car x.cdr x=x)|)
(label simpinfo)

;;;induction

(axiom |∀phi.phi(nil)∧(∀x u.phi(u)⊃phi(x.u))⊃(∀u.phi(u))|)
(label listinduction)

(decl pars (type: |ground*|))
(axiom
 |∀nilcase def.
   ∃fun. ∀pars x u.fun(nil,pars)=nilcase(pars)∧
                   fun(x.u,pars)=def(x,u,fun(u,pars),pars)|)
(label listinductiondef)

(axiom |∀phi.(∀x.atom x ⊃ phi(x))∧(∀x y.phi(x)∧phi(y)⊃phi(x.y))⊃(∀x.phi(x))|)
(label sexpinduction)

(axiom
 |∀atomcase defsexp.
   ∃fun. ∀pars x y.(atom x ⊃ fun(x,pars)=atomcase(x,pars))∧
                   (fun(x.y,pars)=defsexp(x,y,fun(x,pars),fun(y,pars),pars))|)
(label sexpinductiondef)

;;; lists of variable numbers of arguments don't require special treatment,
;;; since we have list types now

(decl list (type: |ground* → ground|) (syntype: constant))
(decl lst (type: |ground*|))
(axiom |∀x.listp(list(x))|)
(label simpinfo)

(axiom |∀x.list(x) = x.nil|)
(label simpinfo)

(axiom |∀lst.listp(list(lst))|)
(label simpinfo)

(axiom |∀x lst.list(x,lst) = x.list(lst)|)
(label simpinfo)

;;; this is lisp's append.  while it can be proved associative, it
;;; is convenient in proofs of other theorems to have it declared
;;; associative.
 
(decl append (type: |ground⊗ground*→ground|) (syntype: constant)
      (associativity: both) (infixname: *) (bindingpower: 840))

(axiom |∀u v.listp(u*v)|)
(label simpinfo) (label listappend)

(axiom |∀x u v.nil*v=v∧(x.u)*v=x.(u*v)|)
(label appendef) (label simpinfo)

(axiom |∀u.u*nil=u|)
(label simpinfo)

(axiom |∀x v.(x.nil)*v=x.v|)
(label simpinfo)

(axiom |∀u v w.u*v*w=u*(v*w)|)
(label apprassoc)

(axiom |∀u v w.u*v*w=(u*v)*w|)
(label applassoc)

;;;map functions on lists

(axiom |∀phi x u.allp(phi,nil)∧
                 (if phi(x) then allp(phi,x.u)=allp(phi,u) else ¬allp(phi,x.u))|)
(label allpdef)

(axiom |∀phi x u.¬somep(phi,nil)∧
                 (if phi(x) then somep(phi,x.u)
			    else somep(phi,x.u)=somep(phi,u))|)
(label somepdef)

(axiom |∀fn x u.mapcar(fn,nil)=nil∧mapcar(fn,x.u)=fn(x).mapcar(fn,u)|)
(label mapcardef)

(decl (alist a0 a1 a2) (type: ground) (sort: alistp))
(axiom |∀alist. listp alist|)
(label simpinfo) 

(axiom |∀alist. ¬null alist ⊃ ¬atom car alist ∧ atom car car alist|)

(axiom |∀xa y alist.alistp (xa.y).alist|)
(label mkalist)

(decl assoc (type:  |ground⊗ground → ground|) (syntype: constant))

(axiom |∀x xa y alist.
         assoc(x,nil)=nil∧
         assoc(x,(xa.y).alist)=(if x=xa then xa.y else assoc(x,alist))|)
(label assocdef)

(axiom |∀x alist.sexp assoc(x,alist)|)
(label simpinfo)

(decl member (type: |ground⊗ground → truthval|) (syntype: constant))

(axiom |∀x y u. ¬member(x,nil)∧member(x,y.u)=(x=y∨member(x,u))|)
(label memberdef)
(save-proofs lispax)
;;; ekl axioms and proofs for permutation functions
(wipe-out)
(get-proofs lispax)
(proof permut)

(decl rac (unaryname: rac) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))
 
(decl rdc (unaryname: rdc) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl snoc (type: |(ground⊗ground)→ground|) (syntype: constant))

(axiom |∀x u.rdc (x.u)=(if null u then nil else x.rdc u)|)
(label rdcdef)

(axiom |∀x u.rac (x.u)=(if null u then x else rac u)|)
(label racdef)

(define snoc |∀x u.snoc(x,u) = u * x.nil|)
(label snocdef)

(decl reverse (unaryname: reverse) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl rev (type: |ground⊗ground→ground|) (syntype: constant))

(define reverse |∀u.reverse u = rev(u,nil)|)
(label reverserev)

(axiom |∀x u v.rev(nil,v)=v∧rev(x.u,v)=rev(u,x.v)|)
(label revdef) (label simpinfo)

(axiom |∀u v.rev(u,v)=reverse u*v|)
(label revprop)

(axiom |∀x u.reverse(nil)=nil∧reverse(x.u)=(reverse u)*(x.nil)|)
(label reversedef) (label simpinfo)

(axiom |∀u.listp reverse u|)
(label reverselist) (label simpinfo)

(axiom |∀x.reverse (x.nil)=x.nil|)
(label simpinfo)

(axiom |∀u.reverse reverse u = u|)
(label simpinfo)
(label reversereverse)

(axiom |∀u v.reverse(u*v) = reverse v * reverse u|)
(label reverseappend)

(decl lcycle (unaryname: lcycle) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(decl rcycle (unaryname: rcycle) (type: |ground→ground|) (syntype: constant)
 (bindingpower: 950))

(define lcycle |∀u.lcycle(u)=if null u then nil else snoc(car u,cdr u)|)
(label lcycledef) (label simpinfo)

(define rcycle |∀u.rcycle(u)=if null u then nil else rac u . rdc u|)
(label rcycledef) (label simpinfo)

(save-proofs permut)
;facts on append
;associativity and termination of append

(get-proofs lispax)

(proof append)
(decl newappend (type: |(ground⊗(ground*))→ground|) (syntype: constant)
  (infixname: **) (bindingpower: 840))

(axiom |∀x u v.nil**u=u∧(x.u)**v=x.(u**v)|)
(label appendef1)

;termination

(ue (phi |λu.∀v.listp (u**v)|) listinduction
    (use appendef1 (mode: t)) simpinfo)
;∀U V.LISTP U ** V
(label listappend1)

;you can now deduce associativity as follows:

(ue (phi |λu.((u**v)**w)=(u**(v**w))|) listinduction
    (use appendef1 (mode: always)) simpinfo listappend1)
;∀U.(U ** V) ** W=U ** (V ** W)
 
;the other nil property

(ue  (phi |λu.u**nil=u|) listinduction
     (use appendef1 (mode: always)) simpinfo listappend1)
;∀U.U ** NIL=U
;facts on reverse: these do the facts mentioned in our meeting for reverse
(wipe-out)
(get-proofs permut)
(proof reverse)

;remove reverse facts from simpinfo so we don't use it accidentally

(unlabel simpinfo reversereverse)
(unlabel simpinfo reverselist)

;termination

(ue (phi |λu.listp reverse u|) listinduction
    (use reversedef (mode: always)) simpinfo)
;∀U.LISTP REVERSE U
(label simpinfo)

;proof of reverseappend

(ue (phi |λu.(reverse (u*v) = reverse(v) * reverse(u))|) listinduction
    (use reversedef (mode: always)) simpinfo)
;(∀X U.REVERSE (U*V)=REVERSE V*REVERSE U⊃
;      REVERSE (U*V)*X.NIL=REVERSE V*REVERSE U*X.NIL)⊃
;(∀U.REVERSE (U*V)=REVERSE V*REVERSE U)
(label step1)

(assume |reverse (u*v)=reverse v*reverse u|)
(label ass)

(tci (ass) |reverse (u*v)*x.nil=reverse v*reverse u*x.nil|
     (use ass (mode: always)) simpinfo))
;REVERSE (U*V)=REVERSE V*REVERSE U⊃REVERSE (U*V)*X.NIL=REVERSE V*REVERSE U*X.NIL
(label step2)

(rw step1 (use step2) simpinfo)
;∀U.REVERSE (U*V)=REVERSE V*REVERSE U

;proof of reversereverse from reverseappend

(ue (phi |λu.reverse (reverse u) = u|) listinduction
    (use (reversedef reverseappend) (mode: always))
    simpinfo)
;∀U.REVERSE (REVERSE U)=U

;proof of reverserev

(ue (phi |λu.∀v.(rev(u,v)=(reverse(u))*v)|) 
    listinduction
    ((use (reversedef revdef) (mode: always))
     (use apprassoc (mode: always)))
    simpinfo)
;∀U V.REV(U,V)=REVERSE U*V
 
(trw permut#reverserev (use *) simpinfo)
;∀U.REVERSE U=REV(U,NIL)
;properties of rac,rdc,snoc,lcycle,rcycle
;the current set of axioms for permut and lispax can be found in lispax.cmd[ekl,jk]
(wipe-out)

(get-proofs permut)
(proof cprops)

(trw |∀x u.snoc(x,u)=reverse(x.reverse(u))|
     (use (snocdef reversedef) (mode: t))
     simpinfo)
;∀X U.SNOC(X,U)=REVERSE (X.REVERSE U)

(trw |∀x u.listp snoc(x,u)| (use * (mode: always)) simpinfo)
;∀X U.LISTP SNOC(X,U)
(label simpinfo)

(ue (phi |λu.rac (u*(x.nil)) = x|) listinduction
    (use racdef (mode: always))
    simpinfo)
;∀U.RAC (U*X.NIL)=X
(label racfact)

(ue (phi |λu.¬NULL U*X.NIL|) listinduction nil simpinfo)
;∀U.¬NULL U*X.NIL
(label simpinfo)

(ue (phi |λu.rdc (u*(x.nil)) = u|) listinduction
    (use rdcdef (mode: always))
    simpinfo)
;∀U.RDC (U*X.NIL)=U
(label rdcfact)

(ue (phi |λu.¬null u ⊃ listp rac u|) listinduction 
    (part 1 (use racdef (mode: always)))
    simpinfo)
;∀U.¬NULL U⊃LISTP RAC U
(label simpinfo)

(ue (phi |λu.¬null u ⊃ listp rdc u|) listinduction 
    (part 1 (use rdcdef (mode: always)))
    simpinfo)
;∀U.¬NULL U⊃LISTP RDC U
(label simpinfo)

(ue (phi |λu.¬null u ⊃ snoc(rac u, rdc u)=u|) listinduction
    (part 1 (use (snocdef racdef rdcdef) (mode: always)))
    simpinfo)
;∀U.¬NULL U⊃SNOC(RAC U,RDC U)=U
(label snocfact)
 
(trw |¬null snoc(x,u)| (open snoc) simpinfo)
;¬NULL SNOC(X,U)
(label simpinfo)

(trw |∀u.listp rcycle u| (use rcycledef (mode: always)) simpinfo)
;∀U.LISTP RCYCLE U
(label simpinfo)

(trw |∀u.listp lcycle u| (use lcycledef (mode: always)) simpinfo)
;∀U.LISTP LCYCLE U
(label simpinfo)

(trw |rcycle lcycle u=u|
     (use (rcycledef lcycledef snocdef racfact rdcfact) (mode: always))
     simpinfo)
;RCYCLE (LCYCLE U)=U
 
(rw snocfact (open snoc) simpinfo)
;∀U.¬NULL U⊃RDC U*RAC U.NIL=U

(trw |(lcycle rcycle u)=u|
     (open rcycle lcycle snoc)
     * simpinfo)
;LCYCLE (RCYCLE U)=U